Specification monotone-set-fixpoint

[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

enrich
   setelems
with
   

   
   
   functions  μ : ((elem → bool) → elem → bool) → elem → bool;
              ν : ((elem → bool) → elem → bool) → elem → bool;
              UN : ((elem → bool) → bool) → elem → bool;
              IS : ((elem → bool) → bool) → elem → bool;
              compl : ((elem → bool) → elem → bool) → (elem → bool) → elem → bool;
             comment: compl(f)(S) = X \ f(X \ S);
   predicates  . ⊆ . : (elem → bool) × (elem → bool);
               monotone : ((elem → bool) → elem → bool);
   
   variables  x : elem;
              x0 : elem;
              x1 : elem;
              S : elem → bool;
              S0 : elem → bool;
              S1 : elem → bool;
              f : (elem → bool) → elem → bool;
              SS : (elem → bool) → bool;
   
   

   

   axioms union-def :  ⊦ UN(SS)(x) ↔ (∃ S. SS(S) ∧ S(x));
          intersection-def :  ⊦ IS(SS)(x) ↔ (∀ S. SS(S) → S(x));
          subseteq-def :  ⊦ S ⊆ S0 ↔ (∀ x. S(x) → S0(x));
          monotone-def :  ⊦ monotone(f) ↔ (∀ S, S0. S ⊆ S0 → f(S) ⊆ f(S0));
          least-prefixpoint-def :  ⊦ μ(f)(x) ↔ (∀ S. f(S) ⊆ S → S(x));
          greatest-prefixpoint-def :  ⊦ ν(f)(x) ↔ ¬ μ(compl(f))(x);
          compl-def :  ⊦ compl(f)(S)(x) ↔ ¬ f(λ x0. ¬ S(x0))(x);

   

   
end enrich